package Main;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

import SATSolver.RecursiveSolver;
import VariablePicker.GreedyPicker;
import VariablePicker.SmallPicker;
import VariablePicker.VariablePicker;


public class Main {
	public static void main(String[] args)
	{
		File file = null;
		FileReader fr = null;
		BufferedReader br = null;
		FileWriter fw = null;
		BufferedWriter bw = null;
		ArrayList<Integer> varRemovedClause = new ArrayList<Integer>();
		
		ArrayList<int[]> clauses = new ArrayList<int[]>();
		try {
			String line = null;
			String [] splitLine = null;
			int [] list = null;
			
			System.out.println(System.getProperty("user.dir"));
			file = new File(System.getProperty("user.dir") + "\\" + args[0]);
			fr = new FileReader(file);
			br = new BufferedReader(fr);
			
			line = br.readLine();
			int i;
			while(line != null) {
				splitLine = line.split(" ");
				list = new int[splitLine.length];
				String tmp;
				for(i = 0; i < list.length; i++) {
					tmp = splitLine[i];
					if(!tmp.isEmpty()) {
						list[i] = Integer.parseInt(tmp);
					}
				}
				list = Clause.formatList(list);

				// if var and -var are in clause then remove clauses
				// make not of variable and make sure to set variable 
				// after setter if var is not set. 
				list = Clause.clauseEliminatorChecker(list, varRemovedClause);

				if(list != null) {
					clauses.add(list);
				}	
				line = br.readLine();
			}
			
			
			SAT sat = new SAT(clauses, new RecursiveSolver(new SmallPicker()));
			
			
			if(sat.canSolve()) {
				String answer = sat.getAnswer(varRemovedClause);
				file = new File(System.getProperty("user.dir") + "\\" + args[0].replace(".txt", "Sol2.txt"));
				fw = new FileWriter(file, false);
				bw = new BufferedWriter(fw);
				bw.write(answer);
				bw.flush();
			} else {
				System.out.println("Can't Solve");
			}
		} catch(IOException e){
			System.out.println(e.getMessage());
		} finally {
			try {
				file = null;
				if(fr != null) fr.close();
				if(br != null) br.close();
				if(fw != null) fw.close();
				if(bw != null) bw.close();
			} catch (IOException e) {}
		}
	}
	
}
